Skip to content

[ new ] Judgement forms and rules #65

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
gallais wants to merge 91 commits into
base: main
Choose a base branch
from
Open

[ new ] Judgement forms and rules #65

gallais wants to merge 91 commits into from

Conversation

@gallais
Copy link
Member

@gallais gallais commented Apr 6, 2023

No description provided.

fredrikNordvallForsberg and others added 30 commits October 5, 2022 16:12
@fredrikNordvallForsberg
[ WIP ] mockup of rules instead of actors, in the middle of the seman…
fe090e4 
…tic specification
@JacquesCarette
snapshot of current work
34582c9
@JacquesCarette
a good day's work on rules and citizens
1303b4b
@maltenmuller
[ WIP ] more design for rules and judg(e)ments
fd8590e
@fredrikNordvallForsberg
[ WIP ] towards representing concrete and abstract rules
de5ea6a
@g-nakov
[ WIP ] towards parsing rules
84aae7f
@g-nakov
[ WIP ] judgement form parsing
39dc5e2
@fredrikNordvallForsberg
[ WIP ] elaborating judgement form declations
65ce92b
@g-nakov
[ wip ] elaboration cont.
0b78635
@g-nakov
[ WIP ] protocol fix, onto syntaxDesc -> semanticsDesc
9e576a8
@g-nakov
[ fix ] impossible error in ssyntaxdesc
218c859
@gallais
[ fix ] back to building
321727a
@gallais
[ minor ] contextual info for judgementform
b4d21e6
@gallais
[ rule ] error reporting for citizen vs. subject mismatch
40bf58e
@gallais
Update Src/Elaboration/Pretty.hs
43244fb
@gallais
[ fix ] better error messages
dc7da1d
@fredrikNordvallForsberg
[ wip ] progress on elaborating judgement forms
b86d8ba
@fredrikNordvallForsberg
better malformed op error
c9f9a9e
@fredrikNordvallForsberg
[ broken ] towards proper Semantics
569b568
@g-nakov
[ wip ] polymorphic headUpData
aaf96a5
@g-nakov
[ wip ] validating semantics via typechecking
b68d0c1
@g-nakov
[ wip ] further progress / regression
734d03c
@g-nakov
[ wip ] small fixes, still not compiling
da55c25
@g-nakov
[ wip ] towards scope checking operator declarations (courtesy of @fred)
40d6997
@g-nakov
[ wip ] fixing (and introducing) errors in elaboration
2394448
@g-nakov
[ wip ] elaboration cont.
d97d818
@g-nakov
[ fix ] errors with pretty printing
2610c52
@g-nakov
[ fix ] some undefined values to get past errors
e4c7774
@gallais
[ more ] isList, sop, itm, (parts of) stm
7de5d7f 
Also, a lot of trailing whitespaces
@g-nakov
[ refactor ] making mangleActors generic over the meta type
c7bb318
gallais and others added 24 commits March 14, 2023 16:44
@gallais
[ fix ] missing range info in smeta
72bfa75
@gallais
[ fix ] printing open terms in error messages
dfe40a6
@fredrikNordvallForsberg
[ fix ] more now working test cases
8a7f8ea
@gallais
[ fix ] bring back clause tracing
433302f
@fredrikNordvallForsberg
towards bringing back judgement declarations
3934124
@gallais
[ bug ] alarm-causing test case
12c57fe
@gallais
[ doc ] matchObjType
40fe9c7
@gallais
[ TODO ] type annotations for operator objects
4ab3a40
@gallais
[ breaking ] insist on binding the obj name in op decl
f5fea2d
@gallais
[ cleanup ] unused imports
570ec1e
@gallais
[ broken ] more uniform operator declaration
64dab28
@gallais
[ fix ] checking judgement form telescopically
7f84d11 
Also fixing Send elaboration
@gallais
[ broken ] subject should become citizen after sub send
cae7116
@fredrikNordvallForsberg
[ test ] update test cases
a564d57
@fredrikNordvallForsberg
[ todo ] add todo
377a10a
@fredrikNordvallForsberg
[ fix ] checking optional patterns in judgements
b76a366
@fredrikNordvallForsberg
[ testing ] excluded directories, and fix README.md
1534176
@gallais
Merge branch 'main' into rules
3732063
@gallais
[ cleanup ] remove filepath printing
a948991
@gallais
[ fix ] disallow matching on the universe
9683c37
@fredrikNordvallForsberg
radicals and types in operators
24ac4dc
@fredrikNordvallForsberg
[ test ] add missing golden file
8d921bb
@fredrikNordvallForsberg
separate examples/stlcRules.act and test/stlcRules.act, which explore…
dd6f862 
…s corner cases
@gallais
[ emacs ] add missing '=>' symbol
bb3998d
@gallais gallais changed the title Judgement forms and rules [ new ] Judgement forms and rules Apr 6, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@gallais @fredrikNordvallForsberg @JacquesCarette @maltenmuller @g-nakov